COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	dirty[f83,jmc] dirty lisp reduced to clean eq and equal
C00005 ENDMK
C⊗;
dirty[f83,jmc] dirty lisp reduced to clean; eq and equal

	Reading all the explanations in the F83 final about why proofs
about compactify cannot be done in our present formalism led to the idea
that maybe they can.  The question is this:  Can we transform a program
that uses eq and a sentence about that program that also involve eq in a
systematic way into an equivalent sentence of pure Lisp theory?

	Here's how it might be done.

	Occurrences of  cons  are replaced by a new  cons; call it
consq.  Occurrences of  eq  are replaced by  equal.  Occurrences of
equal  are replaced by  equalq.  Occurrences  of  car  and   cdr  are
replaced by  carq  and  cdrq  respectively.

	consq  is like  cons,  but includes a gensym so that no
two values are of  consq  equal.  In order to preserve compositionality,
consq  takes a third argument, and the programs are transformed so as
to pass that argument down, suitably transformed.  This is the
process of  gensym-elimination  considered previously.

	carq  and  cdrq  are like  car  and  cdr  operating on the
structures produced by  consq.  They satisfy

	carq(consq(x,y,n)) = x

	cdrq(consq(x,y,n)) = y

	¬atom x  ⊃  (equalq(x,consq(carq x,cdrq x),n))

	consq(x,y,n) = consq(x',y',n') ⊃ x = x' ∧ y = y' ∧ n = n'